While trying to prove some basic properties using coinductive types in Coq, I keep running into the following problem and I cannot get around it. I've distilled the problem into a simple Coq script as follows. The type Tree defines possibly infinite trees with branches labelled with elements of type A. A branch need not be defined for all elements of A. The value Univ is the infinite tree with all A branches always defined. isUniv tests whether a given tree is equal to the Univ. The lemma states that Univ does indeed satisfy isUniv.Parameter A : Set.CoInductive Tree: Set := Node : (A -> option Tree) -> Tree.Definition derv (a : A) (t: Tree): option Tree :=  match t with Node f => f a end.CoFixpoint Univ : Tree := Node (fun _ => Some Univ).CoInductive isUniv : Tree -> Prop :=  isuniv : forall (nf : A -> option Tree) (a : A) (t : Tree),     nf a = Some t ->     isUniv t ->     isUniv (Node nf).Lemma UnivIsUniv : isUniv Univ.Proof.  cofix CH.    (* this application of cofix is fine *)  unfold Univ. Admitted.At this point I give up the proof. The current goal is:CH : isUniv Univ============================isUniv (cofix Univ  : Tree := Node (fun _ : A => Some Univ))I do not know which tactic to apply to eliminate the cofix in the goal to produce (Node something) so that I can apply isuniv. Can anyone help prove this lemma?What are the standard ways of eliminating cofix in such a situation?
Eliminating cofix in Coq proof
coq;proof assistants
You can eliminate cofix using an auxiliary function that pattern matches Tree.Definition TT (t:Tree) :=  match t with    | Node o => Node o  end.Lemma TTid : forall t: Tree, t = TT t.  intro t.  destruct t.  reflexivity.  Qed.Lemma UnivIsUniv : isUniv Univ.Proof.  cofix.  rewrite TTid.  unfold TT.  unfold Univ.You will obtain this goal, which is a step unwinded.  UnivIsUniv : isUniv Univ  ============================   isUniv     (Node        (fun _ : A =>         Some (cofix Univ  : Tree := Node (fun _ : A => Some Univ))))I adapted this technique from http://adam.chlipala.net/cpdt/html/Coinductive.html