proposition: Lemma append_get : forall (A : Set) (n : nat) (l : ilist A n) (x : A), iget (isnoc l x) (nat_to_fin n (PeanoNat.Nat.lt_succ_diag_r n)) = x.
proof: Proof. induction n ; intros. - depelim l. now simp isnoc nat_to_fin iget. - depelim l. simp isnoc nat_to_fin iget. unfold nat_to_fin_obligation_1. etransitivity; [|apply (IHn l)]; do 2 f_equal; apply le_hprop. Qed.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations