proposition: Lemma phi0_ref (i:nat) : refine (phi0 i) = T1.phi0 (\F i).
proof: Proof. reflexivity. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )