fact: Fixpoint Term_requiv (G : ctxt) {t1 t2} (e1 : Term fnvar1 t1) (e2 : Term fnvar2 t2) {struct e1} : match Term_requivT (duplicate_type G) e1 e2, TypeCode_eq_semidec_transparent t1 t2 with | Some reflective_obligation, Some p => to_prop reflective_obligation -> @Term_equiv var1 var2 G t2 (eq_rect _ (@Term _) (unnatize_Term (List.length G) e1) _ p) (unnatize_Term (List.length G) e2) | _, _ => True end.
imports: Coq.Lists.List Coq.Arith.EqNat Coq.Logic.Eqdep_dec Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.SyntaxEquality Fiat.Parsers.Reflective.SyntaxEquivalence Fiat.Common.PointedProp Fiat.Common.OptionFacts Fiat.Common.Prod Fiat.Common.Sigma Fiat.Common